ds:x:Id fp Type, da:k:Knd fp Type, es:ES, i:Id, e1, e2:{e:E| loc(e) = i }.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  da(kind(e))?Top)
 (ks:Knd List, T:Type, z:T, g:(k:{k:Knd| (k  ks) }State(ds)da(k)?TopTT).
 (es-trans-state-from{i:l}(es;ks;g;z;e1;e2)  T) 

latex

Definitions

t  T, KindDeq, x:A. B(x), Knd, (x  l), b, Prop, A, b, , deq-member(eq;x;L), P  Q, P & Q, P  Q, Unit, let x,y,z = a in t(x;y;z), x,y. t(x;y), list_accum(x,a.f(x;a);y;l), es-trans-state-from{i:l}(es;ks;g;z;e1;e2), Top, x. t(x), f(x)?z, State(ds), EqDecider(T), a:A fp B(a), kind(e), valtype(e), loc(e), Id, E, IdDeq, vartype(i;x), ES, es-hist{i:l}(es;e1;e2), event-info(ds;da)

Lemmas

fpf wf, event system wf, es-vartype wf, id-deq wf, es-E wf, Id wf, es-loc wf, es-valtype wf, es-kind wf, fpf-trivial-subtype-top, decl-state wf, fpf-cap wf, top wf, es-hist wf, list accum wf, event-info wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bool wf, bnot wf, not wf, assert wf, l member wf, Knd wf, Kind-deq wf